// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
package org.kframework.compile;

import java.util.HashMap;
import java.util.Map;
import java.util.function.Supplier;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import org.apache.commons.lang3.tuple.Pair;
import org.kframework.mpfr.BigFloat;
import org.kframework.mpfr.BinaryMathContext;

public class FloatBuiltin {

  /* Token cache */
  private static final Map<Pair<BigFloat, Integer>, FloatBuiltin> tokenCache = new HashMap<>();

  /**
   * Returns a {@link FloatBuiltin} representing the given {@link BigFloat} value and the given
   * exponent range, in bits.
   *
   * @param value
   * @return
   */
  public static FloatBuiltin of(BigFloat value, Integer exponent) {
    assert value != null;
    Pair<BigFloat, Integer> key = Pair.of(value, exponent);
    FloatBuiltin floatBuiltin = tokenCache.get(key);
    if (floatBuiltin == null) {
      floatBuiltin = new FloatBuiltin(value, exponent);
      tokenCache.put(key, floatBuiltin);
    }
    return floatBuiltin;
  }

  /**
   * Returns a {@link FloatBuiltin} representing the given {@link double} value.
   *
   * @param value
   * @return
   */
  public static FloatBuiltin of(double value) {
    return of(
        new BigFloat(value, BinaryMathContext.BINARY64), BinaryMathContext.BINARY64_EXPONENT_BITS);
  }

  /**
   * Returns a {@link FloatBuiltin} representing the given {@link float} value.
   *
   * @param value
   * @return
   */
  public static FloatBuiltin of(float value) {
    return of(
        new BigFloat(value, BinaryMathContext.BINARY32), BinaryMathContext.BINARY32_EXPONENT_BITS);
  }

  /**
   * Returns a {@link FloatBuiltin} representing the given {@link String} value.
   *
   * @param value
   * @return
   */
  public static FloatBuiltin of(String value) {
    Pair<BigFloat, Integer> pair = FloatBuiltin.parseKFloat(value);
    return of(pair.getLeft(), pair.getRight());
  }

  private final BigFloat value;
  private final int exponent;

  private FloatBuiltin(BigFloat value, int exponent) {
    this.value = value;
    this.exponent = exponent;
  }

  private static final Pattern precisionAndExponent = Pattern.compile("(.*)[pP](\\d+)[xX](\\d+)");

  public static Pair<BigFloat, Integer> parseKFloat(String s) {
    try {
      Matcher m = precisionAndExponent.matcher(s);
      int precision, exponent;
      String value;
      if (m.matches()) {
        precision = Integer.parseInt(m.group(2));
        exponent = Integer.parseInt(m.group(3));
        value = m.group(1);
      } else if (s.endsWith("f") || s.endsWith("F")) {
        precision = BinaryMathContext.BINARY32.precision;
        exponent = BinaryMathContext.BINARY32_EXPONENT_BITS;
        value = s.substring(0, s.length() - 1);
      } else {
        precision = BinaryMathContext.BINARY64.precision;
        exponent = BinaryMathContext.BINARY64_EXPONENT_BITS;
        if (s.endsWith("d") || s.endsWith("D")) {
          value = s.substring(0, s.length() - 1);
        } else {
          value = s;
        }
      }
      BinaryMathContext mc = new BinaryMathContext(precision, exponent);
      BigFloat result = new BigFloat(value, mc);
      return Pair.of(result, exponent);
    } catch (IllegalArgumentException e) {
      e.printStackTrace();
      throw new NumberFormatException();
    }
  }

  /** Returns a {@link BigFloat} representing the (interpreted) value of the float token. */
  public BigFloat bigFloatValue() {
    return value;
  }

  public float floatValue() {
    return value.floatValue();
  }

  public double doubleValue() {
    return value.doubleValue();
  }

  /** Returns a {@link BinaryMathContext} representing the context to perform arithmetic under. */
  public int exponent() {
    return exponent;
  }

  public BinaryMathContext getMathContext() {
    return new BinaryMathContext(precision(), exponent());
  }

  public int precision() {
    return value.precision();
  }

  /** Returns a {@link String} representing the (uninterpreted) value of the float token. */
  public String value() {
    return printKFloat(value) + printKFloatSuffix(value, exponent);
  }

  /**
   * Return a {@link String} representing the (uninterpreted) value of the numerical float
   * corresponding to the value of the float token.
   */
  public static String printKFloat(BigFloat value) {
    return printKFloat(value, value::toString);
  }

  public static String printKFloat(BigFloat value, Supplier<String> toString) {
    if (value.isInfinite()) {
      if (value.sign()) {
        return "-Infinity";
      } else {
        return "Infinity";
      }
    } else if (value.isNaN()) {
      return "NaN";
    } else {
      return toString.get();
    }
  }

  public static String printKFloatSuffix(BigFloat value, int exponent) {
    return "p" + value.precision() + "x" + exponent;
  }

  @Override
  public int hashCode() {
    return value.hashCode() * 31 + exponent;
  }

  @Override
  public boolean equals(Object object) {
    if (object == null) {
      return false;
    }
    if (!object.getClass().equals(FloatBuiltin.class)) {
      return false;
    }
    FloatBuiltin other = (FloatBuiltin) object;
    if (!value.equals(other.value)) {
      return false;
    }
    return exponent == other.exponent;
  }

  @Override
  public String toString() {
    return value();
  }
}
